Termination w.r.t. Q proof of /tmp/tmpAZBvHi/Ex1_GM03

Termination w.r.t. Q of the following Term Rewriting System could not be shown:

Q restricted rewrite system:
The TRS R consists of the following rules:

active(p(0)) → mark(0)
active(p(s(X))) → mark(X)
active(leq(0, Y)) → mark(true)
active(leq(s(X), 0)) → mark(false)
active(leq(s(X), s(Y))) → mark(leq(X, Y))
active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)
active(diff(X, Y)) → mark(if(leq(X, Y), 0, s(diff(p(X), Y))))
active(p(X)) → p(active(X))
active(s(X)) → s(active(X))
active(leq(X1, X2)) → leq(active(X1), X2)
active(leq(X1, X2)) → leq(X1, active(X2))
active(if(X1, X2, X3)) → if(active(X1), X2, X3)
active(diff(X1, X2)) → diff(active(X1), X2)
active(diff(X1, X2)) → diff(X1, active(X2))
p(mark(X)) → mark(p(X))
s(mark(X)) → mark(s(X))
leq(mark(X1), X2) → mark(leq(X1, X2))
leq(X1, mark(X2)) → mark(leq(X1, X2))
if(mark(X1), X2, X3) → mark(if(X1, X2, X3))
diff(mark(X1), X2) → mark(diff(X1, X2))
diff(X1, mark(X2)) → mark(diff(X1, X2))
proper(p(X)) → p(proper(X))
proper(0) → ok(0)
proper(s(X)) → s(proper(X))
proper(leq(X1, X2)) → leq(proper(X1), proper(X2))
proper(true) → ok(true)
proper(false) → ok(false)
proper(if(X1, X2, X3)) → if(proper(X1), proper(X2), proper(X3))
proper(diff(X1, X2)) → diff(proper(X1), proper(X2))
p(ok(X)) → ok(p(X))
s(ok(X)) → ok(s(X))
leq(ok(X1), ok(X2)) → ok(leq(X1, X2))
if(ok(X1), ok(X2), ok(X3)) → ok(if(X1, X2, X3))
diff(ok(X1), ok(X2)) → ok(diff(X1, X2))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

Q is empty.

↳ QTRS

  ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

active(p(0)) → mark(0)
active(p(s(X))) → mark(X)
active(leq(0, Y)) → mark(true)
active(leq(s(X), 0)) → mark(false)
active(leq(s(X), s(Y))) → mark(leq(X, Y))
active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)
active(diff(X, Y)) → mark(if(leq(X, Y), 0, s(diff(p(X), Y))))
active(p(X)) → p(active(X))
active(s(X)) → s(active(X))
active(leq(X1, X2)) → leq(active(X1), X2)
active(leq(X1, X2)) → leq(X1, active(X2))
active(if(X1, X2, X3)) → if(active(X1), X2, X3)
active(diff(X1, X2)) → diff(active(X1), X2)
active(diff(X1, X2)) → diff(X1, active(X2))
p(mark(X)) → mark(p(X))
s(mark(X)) → mark(s(X))
leq(mark(X1), X2) → mark(leq(X1, X2))
leq(X1, mark(X2)) → mark(leq(X1, X2))
if(mark(X1), X2, X3) → mark(if(X1, X2, X3))
diff(mark(X1), X2) → mark(diff(X1, X2))
diff(X1, mark(X2)) → mark(diff(X1, X2))
proper(p(X)) → p(proper(X))
proper(0) → ok(0)
proper(s(X)) → s(proper(X))
proper(leq(X1, X2)) → leq(proper(X1), proper(X2))
proper(true) → ok(true)
proper(false) → ok(false)
proper(if(X1, X2, X3)) → if(proper(X1), proper(X2), proper(X3))
proper(diff(X1, X2)) → diff(proper(X1), proper(X2))
p(ok(X)) → ok(p(X))
s(ok(X)) → ok(s(X))
leq(ok(X1), ok(X2)) → ok(leq(X1, X2))
if(ok(X1), ok(X2), ok(X3)) → ok(if(X1, X2, X3))
diff(ok(X1), ok(X2)) → ok(diff(X1, X2))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

Q is empty.

Using Dependency Pairs [1,15] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

LEQ(ok(X1), ok(X2)) → LEQ(X1, X2)
ACTIVE(leq(X1, X2)) → ACTIVE(X1)
PROPER(if(X1, X2, X3)) → PROPER(X1)
ACTIVE(diff(X, Y)) → P(X)
LEQ(X1, mark(X2)) → LEQ(X1, X2)
ACTIVE(leq(X1, X2)) → LEQ(active(X1), X2)
PROPER(leq(X1, X2)) → PROPER(X1)
IF(ok(X1), ok(X2), ok(X3)) → IF(X1, X2, X3)
ACTIVE(if(X1, X2, X3)) → IF(active(X1), X2, X3)
ACTIVE(diff(X, Y)) → IF(leq(X, Y), 0, s(diff(p(X), Y)))
ACTIVE(p(X)) → P(active(X))
PROPER(s(X)) → S(proper(X))
P(ok(X)) → P(X)
ACTIVE(diff(X, Y)) → S(diff(p(X), Y))
ACTIVE(diff(X1, X2)) → DIFF(active(X1), X2)
ACTIVE(s(X)) → ACTIVE(X)
DIFF(ok(X1), ok(X2)) → DIFF(X1, X2)
ACTIVE(diff(X1, X2)) → ACTIVE(X2)
PROPER(leq(X1, X2)) → LEQ(proper(X1), proper(X2))
ACTIVE(p(X)) → ACTIVE(X)
S(ok(X)) → S(X)
ACTIVE(leq(X1, X2)) → LEQ(X1, active(X2))
PROPER(p(X)) → PROPER(X)
TOP(mark(X)) → PROPER(X)
P(mark(X)) → P(X)
ACTIVE(diff(X1, X2)) → ACTIVE(X1)
ACTIVE(diff(X, Y)) → LEQ(X, Y)
PROPER(leq(X1, X2)) → PROPER(X2)
LEQ(mark(X1), X2) → LEQ(X1, X2)
TOP(ok(X)) → ACTIVE(X)
PROPER(s(X)) → PROPER(X)
PROPER(if(X1, X2, X3)) → IF(proper(X1), proper(X2), proper(X3))
PROPER(if(X1, X2, X3)) → PROPER(X3)
DIFF(mark(X1), X2) → DIFF(X1, X2)
ACTIVE(if(X1, X2, X3)) → ACTIVE(X1)
ACTIVE(diff(X, Y)) → DIFF(p(X), Y)
PROPER(diff(X1, X2)) → DIFF(proper(X1), proper(X2))
TOP(ok(X)) → TOP(active(X))
S(mark(X)) → S(X)
PROPER(diff(X1, X2)) → PROPER(X2)
PROPER(if(X1, X2, X3)) → PROPER(X2)
ACTIVE(leq(s(X), s(Y))) → LEQ(X, Y)
IF(mark(X1), X2, X3) → IF(X1, X2, X3)
DIFF(X1, mark(X2)) → DIFF(X1, X2)
PROPER(p(X)) → P(proper(X))
ACTIVE(diff(X1, X2)) → DIFF(X1, active(X2))
PROPER(diff(X1, X2)) → PROPER(X1)
ACTIVE(leq(X1, X2)) → ACTIVE(X2)
TOP(mark(X)) → TOP(proper(X))
ACTIVE(s(X)) → S(active(X))

The TRS R consists of the following rules:

active(p(0)) → mark(0)
active(p(s(X))) → mark(X)
active(leq(0, Y)) → mark(true)
active(leq(s(X), 0)) → mark(false)
active(leq(s(X), s(Y))) → mark(leq(X, Y))
active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)
active(diff(X, Y)) → mark(if(leq(X, Y), 0, s(diff(p(X), Y))))
active(p(X)) → p(active(X))
active(s(X)) → s(active(X))
active(leq(X1, X2)) → leq(active(X1), X2)
active(leq(X1, X2)) → leq(X1, active(X2))
active(if(X1, X2, X3)) → if(active(X1), X2, X3)
active(diff(X1, X2)) → diff(active(X1), X2)
active(diff(X1, X2)) → diff(X1, active(X2))
p(mark(X)) → mark(p(X))
s(mark(X)) → mark(s(X))
leq(mark(X1), X2) → mark(leq(X1, X2))
leq(X1, mark(X2)) → mark(leq(X1, X2))
if(mark(X1), X2, X3) → mark(if(X1, X2, X3))
diff(mark(X1), X2) → mark(diff(X1, X2))
diff(X1, mark(X2)) → mark(diff(X1, X2))
proper(p(X)) → p(proper(X))
proper(0) → ok(0)
proper(s(X)) → s(proper(X))
proper(leq(X1, X2)) → leq(proper(X1), proper(X2))
proper(true) → ok(true)
proper(false) → ok(false)
proper(if(X1, X2, X3)) → if(proper(X1), proper(X2), proper(X3))
proper(diff(X1, X2)) → diff(proper(X1), proper(X2))
p(ok(X)) → ok(p(X))
s(ok(X)) → ok(s(X))
leq(ok(X1), ok(X2)) → ok(leq(X1, X2))
if(ok(X1), ok(X2), ok(X3)) → ok(if(X1, X2, X3))
diff(ok(X1), ok(X2)) → ok(diff(X1, X2))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

LEQ(ok(X1), ok(X2)) → LEQ(X1, X2)
ACTIVE(leq(X1, X2)) → ACTIVE(X1)
PROPER(if(X1, X2, X3)) → PROPER(X1)
ACTIVE(diff(X, Y)) → P(X)
LEQ(X1, mark(X2)) → LEQ(X1, X2)
ACTIVE(leq(X1, X2)) → LEQ(active(X1), X2)
PROPER(leq(X1, X2)) → PROPER(X1)
IF(ok(X1), ok(X2), ok(X3)) → IF(X1, X2, X3)
ACTIVE(if(X1, X2, X3)) → IF(active(X1), X2, X3)
ACTIVE(diff(X, Y)) → IF(leq(X, Y), 0, s(diff(p(X), Y)))
ACTIVE(p(X)) → P(active(X))
PROPER(s(X)) → S(proper(X))
P(ok(X)) → P(X)
ACTIVE(diff(X, Y)) → S(diff(p(X), Y))
ACTIVE(diff(X1, X2)) → DIFF(active(X1), X2)
ACTIVE(s(X)) → ACTIVE(X)
DIFF(ok(X1), ok(X2)) → DIFF(X1, X2)
ACTIVE(diff(X1, X2)) → ACTIVE(X2)
PROPER(leq(X1, X2)) → LEQ(proper(X1), proper(X2))
ACTIVE(p(X)) → ACTIVE(X)
S(ok(X)) → S(X)
ACTIVE(leq(X1, X2)) → LEQ(X1, active(X2))
PROPER(p(X)) → PROPER(X)
TOP(mark(X)) → PROPER(X)
P(mark(X)) → P(X)
ACTIVE(diff(X1, X2)) → ACTIVE(X1)
ACTIVE(diff(X, Y)) → LEQ(X, Y)
PROPER(leq(X1, X2)) → PROPER(X2)
LEQ(mark(X1), X2) → LEQ(X1, X2)
TOP(ok(X)) → ACTIVE(X)
PROPER(s(X)) → PROPER(X)
PROPER(if(X1, X2, X3)) → IF(proper(X1), proper(X2), proper(X3))
PROPER(if(X1, X2, X3)) → PROPER(X3)
DIFF(mark(X1), X2) → DIFF(X1, X2)
ACTIVE(if(X1, X2, X3)) → ACTIVE(X1)
ACTIVE(diff(X, Y)) → DIFF(p(X), Y)
PROPER(diff(X1, X2)) → DIFF(proper(X1), proper(X2))
TOP(ok(X)) → TOP(active(X))
S(mark(X)) → S(X)
PROPER(diff(X1, X2)) → PROPER(X2)
PROPER(if(X1, X2, X3)) → PROPER(X2)
ACTIVE(leq(s(X), s(Y))) → LEQ(X, Y)
IF(mark(X1), X2, X3) → IF(X1, X2, X3)
DIFF(X1, mark(X2)) → DIFF(X1, X2)
PROPER(p(X)) → P(proper(X))
ACTIVE(diff(X1, X2)) → DIFF(X1, active(X2))
PROPER(diff(X1, X2)) → PROPER(X1)
ACTIVE(leq(X1, X2)) → ACTIVE(X2)
TOP(mark(X)) → TOP(proper(X))
ACTIVE(s(X)) → S(active(X))

The TRS R consists of the following rules:

active(p(0)) → mark(0)
active(p(s(X))) → mark(X)
active(leq(0, Y)) → mark(true)
active(leq(s(X), 0)) → mark(false)
active(leq(s(X), s(Y))) → mark(leq(X, Y))
active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)
active(diff(X, Y)) → mark(if(leq(X, Y), 0, s(diff(p(X), Y))))
active(p(X)) → p(active(X))
active(s(X)) → s(active(X))
active(leq(X1, X2)) → leq(active(X1), X2)
active(leq(X1, X2)) → leq(X1, active(X2))
active(if(X1, X2, X3)) → if(active(X1), X2, X3)
active(diff(X1, X2)) → diff(active(X1), X2)
active(diff(X1, X2)) → diff(X1, active(X2))
p(mark(X)) → mark(p(X))
s(mark(X)) → mark(s(X))
leq(mark(X1), X2) → mark(leq(X1, X2))
leq(X1, mark(X2)) → mark(leq(X1, X2))
if(mark(X1), X2, X3) → mark(if(X1, X2, X3))
diff(mark(X1), X2) → mark(diff(X1, X2))
diff(X1, mark(X2)) → mark(diff(X1, X2))
proper(p(X)) → p(proper(X))
proper(0) → ok(0)
proper(s(X)) → s(proper(X))
proper(leq(X1, X2)) → leq(proper(X1), proper(X2))
proper(true) → ok(true)
proper(false) → ok(false)
proper(if(X1, X2, X3)) → if(proper(X1), proper(X2), proper(X3))
proper(diff(X1, X2)) → diff(proper(X1), proper(X2))
p(ok(X)) → ok(p(X))
s(ok(X)) → ok(s(X))
leq(ok(X1), ok(X2)) → ok(leq(X1, X2))
if(ok(X1), ok(X2), ok(X3)) → ok(if(X1, X2, X3))
diff(ok(X1), ok(X2)) → ok(diff(X1, X2))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 8 SCCs with 20 less nodes.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

            ↳ UsableRulesProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

DIFF(X1, mark(X2)) → DIFF(X1, X2)
DIFF(ok(X1), ok(X2)) → DIFF(X1, X2)
DIFF(mark(X1), X2) → DIFF(X1, X2)

The TRS R consists of the following rules:

active(p(0)) → mark(0)
active(p(s(X))) → mark(X)
active(leq(0, Y)) → mark(true)
active(leq(s(X), 0)) → mark(false)
active(leq(s(X), s(Y))) → mark(leq(X, Y))
active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)
active(diff(X, Y)) → mark(if(leq(X, Y), 0, s(diff(p(X), Y))))
active(p(X)) → p(active(X))
active(s(X)) → s(active(X))
active(leq(X1, X2)) → leq(active(X1), X2)
active(leq(X1, X2)) → leq(X1, active(X2))
active(if(X1, X2, X3)) → if(active(X1), X2, X3)
active(diff(X1, X2)) → diff(active(X1), X2)
active(diff(X1, X2)) → diff(X1, active(X2))
p(mark(X)) → mark(p(X))
s(mark(X)) → mark(s(X))
leq(mark(X1), X2) → mark(leq(X1, X2))
leq(X1, mark(X2)) → mark(leq(X1, X2))
if(mark(X1), X2, X3) → mark(if(X1, X2, X3))
diff(mark(X1), X2) → mark(diff(X1, X2))
diff(X1, mark(X2)) → mark(diff(X1, X2))
proper(p(X)) → p(proper(X))
proper(0) → ok(0)
proper(s(X)) → s(proper(X))
proper(leq(X1, X2)) → leq(proper(X1), proper(X2))
proper(true) → ok(true)
proper(false) → ok(false)
proper(if(X1, X2, X3)) → if(proper(X1), proper(X2), proper(X3))
proper(diff(X1, X2)) → diff(proper(X1), proper(X2))
p(ok(X)) → ok(p(X))
s(ok(X)) → ok(s(X))
leq(ok(X1), ok(X2)) → ok(leq(X1, X2))
if(ok(X1), ok(X2), ok(X3)) → ok(if(X1, X2, X3))
diff(ok(X1), ok(X2)) → ok(diff(X1, X2))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We can use the usable rules and reduction pair processor [15] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its argument. Then, we can delete all non-usable rules [17] from R.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QDPSizeChangeProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

DIFF(X1, mark(X2)) → DIFF(X1, X2)
DIFF(ok(X1), ok(X2)) → DIFF(X1, X2)
DIFF(mark(X1), X2) → DIFF(X1, X2)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

DIFF(X1, mark(X2)) → DIFF(X1, X2)
The graph contains the following edges 1 >= 1, 2 > 2
DIFF(ok(X1), ok(X2)) → DIFF(X1, X2)
The graph contains the following edges 1 > 1, 2 > 2
DIFF(mark(X1), X2) → DIFF(X1, X2)
The graph contains the following edges 1 > 1, 2 >= 2

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

IF(mark(X1), X2, X3) → IF(X1, X2, X3)
IF(ok(X1), ok(X2), ok(X3)) → IF(X1, X2, X3)

The TRS R consists of the following rules:

active(p(0)) → mark(0)
active(p(s(X))) → mark(X)
active(leq(0, Y)) → mark(true)
active(leq(s(X), 0)) → mark(false)
active(leq(s(X), s(Y))) → mark(leq(X, Y))
active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)
active(diff(X, Y)) → mark(if(leq(X, Y), 0, s(diff(p(X), Y))))
active(p(X)) → p(active(X))
active(s(X)) → s(active(X))
active(leq(X1, X2)) → leq(active(X1), X2)
active(leq(X1, X2)) → leq(X1, active(X2))
active(if(X1, X2, X3)) → if(active(X1), X2, X3)
active(diff(X1, X2)) → diff(active(X1), X2)
active(diff(X1, X2)) → diff(X1, active(X2))
p(mark(X)) → mark(p(X))
s(mark(X)) → mark(s(X))
leq(mark(X1), X2) → mark(leq(X1, X2))
leq(X1, mark(X2)) → mark(leq(X1, X2))
if(mark(X1), X2, X3) → mark(if(X1, X2, X3))
diff(mark(X1), X2) → mark(diff(X1, X2))
diff(X1, mark(X2)) → mark(diff(X1, X2))
proper(p(X)) → p(proper(X))
proper(0) → ok(0)
proper(s(X)) → s(proper(X))
proper(leq(X1, X2)) → leq(proper(X1), proper(X2))
proper(true) → ok(true)
proper(false) → ok(false)
proper(if(X1, X2, X3)) → if(proper(X1), proper(X2), proper(X3))
proper(diff(X1, X2)) → diff(proper(X1), proper(X2))
p(ok(X)) → ok(p(X))
s(ok(X)) → ok(s(X))
leq(ok(X1), ok(X2)) → ok(leq(X1, X2))
if(ok(X1), ok(X2), ok(X3)) → ok(if(X1, X2, X3))
diff(ok(X1), ok(X2)) → ok(diff(X1, X2))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QDPSizeChangeProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

IF(mark(X1), X2, X3) → IF(X1, X2, X3)
IF(ok(X1), ok(X2), ok(X3)) → IF(X1, X2, X3)

From the DPs we obtained the following set of size-change graphs:

IF(mark(X1), X2, X3) → IF(X1, X2, X3)
The graph contains the following edges 1 > 1, 2 >= 2, 3 >= 3
IF(ok(X1), ok(X2), ok(X3)) → IF(X1, X2, X3)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

LEQ(ok(X1), ok(X2)) → LEQ(X1, X2)
LEQ(X1, mark(X2)) → LEQ(X1, X2)
LEQ(mark(X1), X2) → LEQ(X1, X2)

The TRS R consists of the following rules:

active(p(0)) → mark(0)
active(p(s(X))) → mark(X)
active(leq(0, Y)) → mark(true)
active(leq(s(X), 0)) → mark(false)
active(leq(s(X), s(Y))) → mark(leq(X, Y))
active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)
active(diff(X, Y)) → mark(if(leq(X, Y), 0, s(diff(p(X), Y))))
active(p(X)) → p(active(X))
active(s(X)) → s(active(X))
active(leq(X1, X2)) → leq(active(X1), X2)
active(leq(X1, X2)) → leq(X1, active(X2))
active(if(X1, X2, X3)) → if(active(X1), X2, X3)
active(diff(X1, X2)) → diff(active(X1), X2)
active(diff(X1, X2)) → diff(X1, active(X2))
p(mark(X)) → mark(p(X))
s(mark(X)) → mark(s(X))
leq(mark(X1), X2) → mark(leq(X1, X2))
leq(X1, mark(X2)) → mark(leq(X1, X2))
if(mark(X1), X2, X3) → mark(if(X1, X2, X3))
diff(mark(X1), X2) → mark(diff(X1, X2))
diff(X1, mark(X2)) → mark(diff(X1, X2))
proper(p(X)) → p(proper(X))
proper(0) → ok(0)
proper(s(X)) → s(proper(X))
proper(leq(X1, X2)) → leq(proper(X1), proper(X2))
proper(true) → ok(true)
proper(false) → ok(false)
proper(if(X1, X2, X3)) → if(proper(X1), proper(X2), proper(X3))
proper(diff(X1, X2)) → diff(proper(X1), proper(X2))
p(ok(X)) → ok(p(X))
s(ok(X)) → ok(s(X))
leq(ok(X1), ok(X2)) → ok(leq(X1, X2))
if(ok(X1), ok(X2), ok(X3)) → ok(if(X1, X2, X3))
diff(ok(X1), ok(X2)) → ok(diff(X1, X2))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QDPSizeChangeProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

LEQ(ok(X1), ok(X2)) → LEQ(X1, X2)
LEQ(X1, mark(X2)) → LEQ(X1, X2)
LEQ(mark(X1), X2) → LEQ(X1, X2)

From the DPs we obtained the following set of size-change graphs:

LEQ(ok(X1), ok(X2)) → LEQ(X1, X2)
The graph contains the following edges 1 > 1, 2 > 2
LEQ(X1, mark(X2)) → LEQ(X1, X2)
The graph contains the following edges 1 >= 1, 2 > 2
LEQ(mark(X1), X2) → LEQ(X1, X2)
The graph contains the following edges 1 > 1, 2 >= 2

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

S(ok(X)) → S(X)
S(mark(X)) → S(X)

The TRS R consists of the following rules:

active(p(0)) → mark(0)
active(p(s(X))) → mark(X)
active(leq(0, Y)) → mark(true)
active(leq(s(X), 0)) → mark(false)
active(leq(s(X), s(Y))) → mark(leq(X, Y))
active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)
active(diff(X, Y)) → mark(if(leq(X, Y), 0, s(diff(p(X), Y))))
active(p(X)) → p(active(X))
active(s(X)) → s(active(X))
active(leq(X1, X2)) → leq(active(X1), X2)
active(leq(X1, X2)) → leq(X1, active(X2))
active(if(X1, X2, X3)) → if(active(X1), X2, X3)
active(diff(X1, X2)) → diff(active(X1), X2)
active(diff(X1, X2)) → diff(X1, active(X2))
p(mark(X)) → mark(p(X))
s(mark(X)) → mark(s(X))
leq(mark(X1), X2) → mark(leq(X1, X2))
leq(X1, mark(X2)) → mark(leq(X1, X2))
if(mark(X1), X2, X3) → mark(if(X1, X2, X3))
diff(mark(X1), X2) → mark(diff(X1, X2))
diff(X1, mark(X2)) → mark(diff(X1, X2))
proper(p(X)) → p(proper(X))
proper(0) → ok(0)
proper(s(X)) → s(proper(X))
proper(leq(X1, X2)) → leq(proper(X1), proper(X2))
proper(true) → ok(true)
proper(false) → ok(false)
proper(if(X1, X2, X3)) → if(proper(X1), proper(X2), proper(X3))
proper(diff(X1, X2)) → diff(proper(X1), proper(X2))
p(ok(X)) → ok(p(X))
s(ok(X)) → ok(s(X))
leq(ok(X1), ok(X2)) → ok(leq(X1, X2))
if(ok(X1), ok(X2), ok(X3)) → ok(if(X1, X2, X3))
diff(ok(X1), ok(X2)) → ok(diff(X1, X2))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QDPSizeChangeProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

S(ok(X)) → S(X)
S(mark(X)) → S(X)

From the DPs we obtained the following set of size-change graphs:

S(ok(X)) → S(X)
The graph contains the following edges 1 > 1
S(mark(X)) → S(X)
The graph contains the following edges 1 > 1

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

P(mark(X)) → P(X)
P(ok(X)) → P(X)

The TRS R consists of the following rules:

active(p(0)) → mark(0)
active(p(s(X))) → mark(X)
active(leq(0, Y)) → mark(true)
active(leq(s(X), 0)) → mark(false)
active(leq(s(X), s(Y))) → mark(leq(X, Y))
active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)
active(diff(X, Y)) → mark(if(leq(X, Y), 0, s(diff(p(X), Y))))
active(p(X)) → p(active(X))
active(s(X)) → s(active(X))
active(leq(X1, X2)) → leq(active(X1), X2)
active(leq(X1, X2)) → leq(X1, active(X2))
active(if(X1, X2, X3)) → if(active(X1), X2, X3)
active(diff(X1, X2)) → diff(active(X1), X2)
active(diff(X1, X2)) → diff(X1, active(X2))
p(mark(X)) → mark(p(X))
s(mark(X)) → mark(s(X))
leq(mark(X1), X2) → mark(leq(X1, X2))
leq(X1, mark(X2)) → mark(leq(X1, X2))
if(mark(X1), X2, X3) → mark(if(X1, X2, X3))
diff(mark(X1), X2) → mark(diff(X1, X2))
diff(X1, mark(X2)) → mark(diff(X1, X2))
proper(p(X)) → p(proper(X))
proper(0) → ok(0)
proper(s(X)) → s(proper(X))
proper(leq(X1, X2)) → leq(proper(X1), proper(X2))
proper(true) → ok(true)
proper(false) → ok(false)
proper(if(X1, X2, X3)) → if(proper(X1), proper(X2), proper(X3))
proper(diff(X1, X2)) → diff(proper(X1), proper(X2))
p(ok(X)) → ok(p(X))
s(ok(X)) → ok(s(X))
leq(ok(X1), ok(X2)) → ok(leq(X1, X2))
if(ok(X1), ok(X2), ok(X3)) → ok(if(X1, X2, X3))
diff(ok(X1), ok(X2)) → ok(diff(X1, X2))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QDPSizeChangeProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

P(mark(X)) → P(X)
P(ok(X)) → P(X)

From the DPs we obtained the following set of size-change graphs:

P(mark(X)) → P(X)
The graph contains the following edges 1 > 1
P(ok(X)) → P(X)
The graph contains the following edges 1 > 1

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

PROPER(diff(X1, X2)) → PROPER(X2)
PROPER(p(X)) → PROPER(X)
PROPER(if(X1, X2, X3)) → PROPER(X2)
PROPER(s(X)) → PROPER(X)
PROPER(if(X1, X2, X3)) → PROPER(X3)
PROPER(diff(X1, X2)) → PROPER(X1)
PROPER(leq(X1, X2)) → PROPER(X2)
PROPER(if(X1, X2, X3)) → PROPER(X1)
PROPER(leq(X1, X2)) → PROPER(X1)

The TRS R consists of the following rules:

active(p(0)) → mark(0)
active(p(s(X))) → mark(X)
active(leq(0, Y)) → mark(true)
active(leq(s(X), 0)) → mark(false)
active(leq(s(X), s(Y))) → mark(leq(X, Y))
active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)
active(diff(X, Y)) → mark(if(leq(X, Y), 0, s(diff(p(X), Y))))
active(p(X)) → p(active(X))
active(s(X)) → s(active(X))
active(leq(X1, X2)) → leq(active(X1), X2)
active(leq(X1, X2)) → leq(X1, active(X2))
active(if(X1, X2, X3)) → if(active(X1), X2, X3)
active(diff(X1, X2)) → diff(active(X1), X2)
active(diff(X1, X2)) → diff(X1, active(X2))
p(mark(X)) → mark(p(X))
s(mark(X)) → mark(s(X))
leq(mark(X1), X2) → mark(leq(X1, X2))
leq(X1, mark(X2)) → mark(leq(X1, X2))
if(mark(X1), X2, X3) → mark(if(X1, X2, X3))
diff(mark(X1), X2) → mark(diff(X1, X2))
diff(X1, mark(X2)) → mark(diff(X1, X2))
proper(p(X)) → p(proper(X))
proper(0) → ok(0)
proper(s(X)) → s(proper(X))
proper(leq(X1, X2)) → leq(proper(X1), proper(X2))
proper(true) → ok(true)
proper(false) → ok(false)
proper(if(X1, X2, X3)) → if(proper(X1), proper(X2), proper(X3))
proper(diff(X1, X2)) → diff(proper(X1), proper(X2))
p(ok(X)) → ok(p(X))
s(ok(X)) → ok(s(X))
leq(ok(X1), ok(X2)) → ok(leq(X1, X2))
if(ok(X1), ok(X2), ok(X3)) → ok(if(X1, X2, X3))
diff(ok(X1), ok(X2)) → ok(diff(X1, X2))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QDPSizeChangeProof

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

PROPER(diff(X1, X2)) → PROPER(X2)
PROPER(p(X)) → PROPER(X)
PROPER(s(X)) → PROPER(X)
PROPER(if(X1, X2, X3)) → PROPER(X2)
PROPER(if(X1, X2, X3)) → PROPER(X3)
PROPER(diff(X1, X2)) → PROPER(X1)
PROPER(leq(X1, X2)) → PROPER(X2)
PROPER(leq(X1, X2)) → PROPER(X1)
PROPER(if(X1, X2, X3)) → PROPER(X1)

From the DPs we obtained the following set of size-change graphs:

PROPER(diff(X1, X2)) → PROPER(X2)
The graph contains the following edges 1 > 1
PROPER(p(X)) → PROPER(X)
The graph contains the following edges 1 > 1
PROPER(if(X1, X2, X3)) → PROPER(X2)
The graph contains the following edges 1 > 1
PROPER(s(X)) → PROPER(X)
The graph contains the following edges 1 > 1
PROPER(if(X1, X2, X3)) → PROPER(X3)
The graph contains the following edges 1 > 1
PROPER(diff(X1, X2)) → PROPER(X1)
The graph contains the following edges 1 > 1
PROPER(leq(X1, X2)) → PROPER(X2)
The graph contains the following edges 1 > 1
PROPER(if(X1, X2, X3)) → PROPER(X1)
The graph contains the following edges 1 > 1
PROPER(leq(X1, X2)) → PROPER(X1)
The graph contains the following edges 1 > 1

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

ACTIVE(s(X)) → ACTIVE(X)
ACTIVE(diff(X1, X2)) → ACTIVE(X1)
ACTIVE(diff(X1, X2)) → ACTIVE(X2)
ACTIVE(leq(X1, X2)) → ACTIVE(X2)
ACTIVE(leq(X1, X2)) → ACTIVE(X1)
ACTIVE(if(X1, X2, X3)) → ACTIVE(X1)
ACTIVE(p(X)) → ACTIVE(X)

The TRS R consists of the following rules:

active(p(0)) → mark(0)
active(p(s(X))) → mark(X)
active(leq(0, Y)) → mark(true)
active(leq(s(X), 0)) → mark(false)
active(leq(s(X), s(Y))) → mark(leq(X, Y))
active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)
active(diff(X, Y)) → mark(if(leq(X, Y), 0, s(diff(p(X), Y))))
active(p(X)) → p(active(X))
active(s(X)) → s(active(X))
active(leq(X1, X2)) → leq(active(X1), X2)
active(leq(X1, X2)) → leq(X1, active(X2))
active(if(X1, X2, X3)) → if(active(X1), X2, X3)
active(diff(X1, X2)) → diff(active(X1), X2)
active(diff(X1, X2)) → diff(X1, active(X2))
p(mark(X)) → mark(p(X))
s(mark(X)) → mark(s(X))
leq(mark(X1), X2) → mark(leq(X1, X2))
leq(X1, mark(X2)) → mark(leq(X1, X2))
if(mark(X1), X2, X3) → mark(if(X1, X2, X3))
diff(mark(X1), X2) → mark(diff(X1, X2))
diff(X1, mark(X2)) → mark(diff(X1, X2))
proper(p(X)) → p(proper(X))
proper(0) → ok(0)
proper(s(X)) → s(proper(X))
proper(leq(X1, X2)) → leq(proper(X1), proper(X2))
proper(true) → ok(true)
proper(false) → ok(false)
proper(if(X1, X2, X3)) → if(proper(X1), proper(X2), proper(X3))
proper(diff(X1, X2)) → diff(proper(X1), proper(X2))
p(ok(X)) → ok(p(X))
s(ok(X)) → ok(s(X))
leq(ok(X1), ok(X2)) → ok(leq(X1, X2))
if(ok(X1), ok(X2), ok(X3)) → ok(if(X1, X2, X3))
diff(ok(X1), ok(X2)) → ok(diff(X1, X2))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QDPSizeChangeProof

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

ACTIVE(s(X)) → ACTIVE(X)
ACTIVE(diff(X1, X2)) → ACTIVE(X1)
ACTIVE(leq(X1, X2)) → ACTIVE(X1)
ACTIVE(leq(X1, X2)) → ACTIVE(X2)
ACTIVE(diff(X1, X2)) → ACTIVE(X2)
ACTIVE(if(X1, X2, X3)) → ACTIVE(X1)
ACTIVE(p(X)) → ACTIVE(X)

From the DPs we obtained the following set of size-change graphs:

ACTIVE(s(X)) → ACTIVE(X)
The graph contains the following edges 1 > 1
ACTIVE(diff(X1, X2)) → ACTIVE(X1)
The graph contains the following edges 1 > 1
ACTIVE(diff(X1, X2)) → ACTIVE(X2)
The graph contains the following edges 1 > 1
ACTIVE(leq(X1, X2)) → ACTIVE(X2)
The graph contains the following edges 1 > 1
ACTIVE(leq(X1, X2)) → ACTIVE(X1)
The graph contains the following edges 1 > 1
ACTIVE(if(X1, X2, X3)) → ACTIVE(X1)
The graph contains the following edges 1 > 1
ACTIVE(p(X)) → ACTIVE(X)
The graph contains the following edges 1 > 1

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesReductionPairsProof

Q DP problem:
The TRS P consists of the following rules:

TOP(mark(X)) → TOP(proper(X))
TOP(ok(X)) → TOP(active(X))

The TRS R consists of the following rules:

active(p(0)) → mark(0)
active(p(s(X))) → mark(X)
active(leq(0, Y)) → mark(true)
active(leq(s(X), 0)) → mark(false)
active(leq(s(X), s(Y))) → mark(leq(X, Y))
active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)
active(diff(X, Y)) → mark(if(leq(X, Y), 0, s(diff(p(X), Y))))
active(p(X)) → p(active(X))
active(s(X)) → s(active(X))
active(leq(X1, X2)) → leq(active(X1), X2)
active(leq(X1, X2)) → leq(X1, active(X2))
active(if(X1, X2, X3)) → if(active(X1), X2, X3)
active(diff(X1, X2)) → diff(active(X1), X2)
active(diff(X1, X2)) → diff(X1, active(X2))
p(mark(X)) → mark(p(X))
s(mark(X)) → mark(s(X))
leq(mark(X1), X2) → mark(leq(X1, X2))
leq(X1, mark(X2)) → mark(leq(X1, X2))
if(mark(X1), X2, X3) → mark(if(X1, X2, X3))
diff(mark(X1), X2) → mark(diff(X1, X2))
diff(X1, mark(X2)) → mark(diff(X1, X2))
proper(p(X)) → p(proper(X))
proper(0) → ok(0)
proper(s(X)) → s(proper(X))
proper(leq(X1, X2)) → leq(proper(X1), proper(X2))
proper(true) → ok(true)
proper(false) → ok(false)
proper(if(X1, X2, X3)) → if(proper(X1), proper(X2), proper(X3))
proper(diff(X1, X2)) → diff(proper(X1), proper(X2))
p(ok(X)) → ok(p(X))
s(ok(X)) → ok(s(X))
leq(ok(X1), ok(X2)) → ok(leq(X1, X2))
if(ok(X1), ok(X2), ok(X3)) → ok(if(X1, X2, X3))
diff(ok(X1), ok(X2)) → ok(diff(X1, X2))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the usable rules with reduction pair processor [15] with a polynomial ordering [25], all dependency pairs and the corresponding usable rules [17] can be oriented non-strictly. All non-usable rules are removed, and those dependency pairs and usable rules that have been oriented strictly or contain non-usable symbols in their left-hand side are removed as well.

No dependency pairs are removed.

No rules are removed from R.

Used ordering: POLO with Polynomial interpretation [25]:

POL(0) = 0
POL(TOP(x₁)) = 2·x₁
POL(active(x₁)) = 2·x₁
POL(diff(x₁, x₂)) = 2·x₁ + x₂
POL(false) = 0
POL(if(x₁, x₂, x₃)) = x₁ + 2·x₂ + x₃
POL(leq(x₁, x₂)) = x₁ + x₂
POL(mark(x₁)) = x₁
POL(ok(x₁)) = 2·x₁
POL(p(x₁)) = x₁
POL(proper(x₁)) = x₁
POL(s(x₁)) = x₁
POL(true) = 0

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesReductionPairsProof

              ↳ QDP

                ↳ Narrowing

Q DP problem:
The TRS P consists of the following rules:

TOP(mark(X)) → TOP(proper(X))
TOP(ok(X)) → TOP(active(X))

The TRS R consists of the following rules:

active(p(0)) → mark(0)
active(p(s(X))) → mark(X)
active(leq(0, Y)) → mark(true)
active(leq(s(X), 0)) → mark(false)
active(leq(s(X), s(Y))) → mark(leq(X, Y))
active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)
active(diff(X, Y)) → mark(if(leq(X, Y), 0, s(diff(p(X), Y))))
active(p(X)) → p(active(X))
active(s(X)) → s(active(X))
active(leq(X1, X2)) → leq(active(X1), X2)
active(leq(X1, X2)) → leq(X1, active(X2))
active(if(X1, X2, X3)) → if(active(X1), X2, X3)
active(diff(X1, X2)) → diff(active(X1), X2)
active(diff(X1, X2)) → diff(X1, active(X2))
diff(mark(X1), X2) → mark(diff(X1, X2))
diff(X1, mark(X2)) → mark(diff(X1, X2))
diff(ok(X1), ok(X2)) → ok(diff(X1, X2))
if(mark(X1), X2, X3) → mark(if(X1, X2, X3))
if(ok(X1), ok(X2), ok(X3)) → ok(if(X1, X2, X3))
leq(mark(X1), X2) → mark(leq(X1, X2))
leq(X1, mark(X2)) → mark(leq(X1, X2))
leq(ok(X1), ok(X2)) → ok(leq(X1, X2))
s(mark(X)) → mark(s(X))
s(ok(X)) → ok(s(X))
p(mark(X)) → mark(p(X))
p(ok(X)) → ok(p(X))
proper(p(X)) → p(proper(X))
proper(0) → ok(0)
proper(s(X)) → s(proper(X))
proper(leq(X1, X2)) → leq(proper(X1), proper(X2))
proper(true) → ok(true)
proper(false) → ok(false)
proper(if(X1, X2, X3)) → if(proper(X1), proper(X2), proper(X3))
proper(diff(X1, X2)) → diff(proper(X1), proper(X2))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule TOP(mark(X)) → TOP(proper(X)) at position [0] we obtained the following new rules:

TOP(mark(if(x0, x1, x2))) → TOP(if(proper(x0), proper(x1), proper(x2)))
TOP(mark(leq(x0, x1))) → TOP(leq(proper(x0), proper(x1)))
TOP(mark(s(x0))) → TOP(s(proper(x0)))
TOP(mark(true)) → TOP(ok(true))
TOP(mark(diff(x0, x1))) → TOP(diff(proper(x0), proper(x1)))
TOP(mark(p(x0))) → TOP(p(proper(x0)))
TOP(mark(0)) → TOP(ok(0))
TOP(mark(false)) → TOP(ok(false))

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesReductionPairsProof

              ↳ QDP

                ↳ Narrowing

                  ↳ QDP

                    ↳ Narrowing

Q DP problem:
The TRS P consists of the following rules:

TOP(mark(if(x0, x1, x2))) → TOP(if(proper(x0), proper(x1), proper(x2)))
TOP(mark(leq(x0, x1))) → TOP(leq(proper(x0), proper(x1)))
TOP(mark(s(x0))) → TOP(s(proper(x0)))
TOP(mark(true)) → TOP(ok(true))
TOP(mark(diff(x0, x1))) → TOP(diff(proper(x0), proper(x1)))
TOP(mark(false)) → TOP(ok(false))
TOP(mark(0)) → TOP(ok(0))
TOP(mark(p(x0))) → TOP(p(proper(x0)))
TOP(ok(X)) → TOP(active(X))

The TRS R consists of the following rules:

active(p(0)) → mark(0)
active(p(s(X))) → mark(X)
active(leq(0, Y)) → mark(true)
active(leq(s(X), 0)) → mark(false)
active(leq(s(X), s(Y))) → mark(leq(X, Y))
active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)
active(diff(X, Y)) → mark(if(leq(X, Y), 0, s(diff(p(X), Y))))
active(p(X)) → p(active(X))
active(s(X)) → s(active(X))
active(leq(X1, X2)) → leq(active(X1), X2)
active(leq(X1, X2)) → leq(X1, active(X2))
active(if(X1, X2, X3)) → if(active(X1), X2, X3)
active(diff(X1, X2)) → diff(active(X1), X2)
active(diff(X1, X2)) → diff(X1, active(X2))
diff(mark(X1), X2) → mark(diff(X1, X2))
diff(X1, mark(X2)) → mark(diff(X1, X2))
diff(ok(X1), ok(X2)) → ok(diff(X1, X2))
if(mark(X1), X2, X3) → mark(if(X1, X2, X3))
if(ok(X1), ok(X2), ok(X3)) → ok(if(X1, X2, X3))
leq(mark(X1), X2) → mark(leq(X1, X2))
leq(X1, mark(X2)) → mark(leq(X1, X2))
leq(ok(X1), ok(X2)) → ok(leq(X1, X2))
s(mark(X)) → mark(s(X))
s(ok(X)) → ok(s(X))
p(mark(X)) → mark(p(X))
p(ok(X)) → ok(p(X))
proper(p(X)) → p(proper(X))
proper(0) → ok(0)
proper(s(X)) → s(proper(X))
proper(leq(X1, X2)) → leq(proper(X1), proper(X2))
proper(true) → ok(true)
proper(false) → ok(false)
proper(if(X1, X2, X3)) → if(proper(X1), proper(X2), proper(X3))
proper(diff(X1, X2)) → diff(proper(X1), proper(X2))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule TOP(ok(X)) → TOP(active(X)) at position [0] we obtained the following new rules:

TOP(ok(diff(x0, x1))) → TOP(diff(active(x0), x1))
TOP(ok(diff(x0, x1))) → TOP(diff(x0, active(x1)))
TOP(ok(p(s(x0)))) → TOP(mark(x0))
TOP(ok(leq(x0, x1))) → TOP(leq(active(x0), x1))
TOP(ok(if(x0, x1, x2))) → TOP(if(active(x0), x1, x2))
TOP(ok(if(false, x0, x1))) → TOP(mark(x1))
TOP(ok(leq(x0, x1))) → TOP(leq(x0, active(x1)))
TOP(ok(leq(0, x0))) → TOP(mark(true))
TOP(ok(leq(s(x0), 0))) → TOP(mark(false))
TOP(ok(leq(s(x0), s(x1)))) → TOP(mark(leq(x0, x1)))
TOP(ok(s(x0))) → TOP(s(active(x0)))
TOP(ok(diff(x0, x1))) → TOP(mark(if(leq(x0, x1), 0, s(diff(p(x0), x1)))))
TOP(ok(if(true, x0, x1))) → TOP(mark(x0))
TOP(ok(p(x0))) → TOP(p(active(x0)))
TOP(ok(p(0))) → TOP(mark(0))

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesReductionPairsProof

              ↳ QDP

                ↳ Narrowing

                  ↳ QDP

                    ↳ Narrowing

                      ↳ QDP

                        ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

TOP(ok(diff(x0, x1))) → TOP(diff(active(x0), x1))
TOP(ok(diff(x0, x1))) → TOP(diff(x0, active(x1)))
TOP(ok(p(s(x0)))) → TOP(mark(x0))
TOP(mark(s(x0))) → TOP(s(proper(x0)))
TOP(ok(leq(x0, x1))) → TOP(leq(active(x0), x1))
TOP(ok(if(x0, x1, x2))) → TOP(if(active(x0), x1, x2))
TOP(ok(leq(x0, x1))) → TOP(leq(x0, active(x1)))
TOP(ok(if(false, x0, x1))) → TOP(mark(x1))
TOP(ok(leq(0, x0))) → TOP(mark(true))
TOP(mark(diff(x0, x1))) → TOP(diff(proper(x0), proper(x1)))
TOP(mark(false)) → TOP(ok(false))
TOP(mark(0)) → TOP(ok(0))
TOP(mark(p(x0))) → TOP(p(proper(x0)))
TOP(ok(leq(s(x0), 0))) → TOP(mark(false))
TOP(ok(leq(s(x0), s(x1)))) → TOP(mark(leq(x0, x1)))
TOP(ok(s(x0))) → TOP(s(active(x0)))
TOP(ok(diff(x0, x1))) → TOP(mark(if(leq(x0, x1), 0, s(diff(p(x0), x1)))))
TOP(mark(if(x0, x1, x2))) → TOP(if(proper(x0), proper(x1), proper(x2)))
TOP(mark(leq(x0, x1))) → TOP(leq(proper(x0), proper(x1)))
TOP(ok(p(x0))) → TOP(p(active(x0)))
TOP(ok(if(true, x0, x1))) → TOP(mark(x0))
TOP(mark(true)) → TOP(ok(true))
TOP(ok(p(0))) → TOP(mark(0))

The TRS R consists of the following rules:

active(p(0)) → mark(0)
active(p(s(X))) → mark(X)
active(leq(0, Y)) → mark(true)
active(leq(s(X), 0)) → mark(false)
active(leq(s(X), s(Y))) → mark(leq(X, Y))
active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)
active(diff(X, Y)) → mark(if(leq(X, Y), 0, s(diff(p(X), Y))))
active(p(X)) → p(active(X))
active(s(X)) → s(active(X))
active(leq(X1, X2)) → leq(active(X1), X2)
active(leq(X1, X2)) → leq(X1, active(X2))
active(if(X1, X2, X3)) → if(active(X1), X2, X3)
active(diff(X1, X2)) → diff(active(X1), X2)
active(diff(X1, X2)) → diff(X1, active(X2))
diff(mark(X1), X2) → mark(diff(X1, X2))
diff(X1, mark(X2)) → mark(diff(X1, X2))
diff(ok(X1), ok(X2)) → ok(diff(X1, X2))
if(mark(X1), X2, X3) → mark(if(X1, X2, X3))
if(ok(X1), ok(X2), ok(X3)) → ok(if(X1, X2, X3))
leq(mark(X1), X2) → mark(leq(X1, X2))
leq(X1, mark(X2)) → mark(leq(X1, X2))
leq(ok(X1), ok(X2)) → ok(leq(X1, X2))
s(mark(X)) → mark(s(X))
s(ok(X)) → ok(s(X))
p(mark(X)) → mark(p(X))
p(ok(X)) → ok(p(X))
proper(p(X)) → p(proper(X))
proper(0) → ok(0)
proper(s(X)) → s(proper(X))
proper(leq(X1, X2)) → leq(proper(X1), proper(X2))
proper(true) → ok(true)
proper(false) → ok(false)
proper(if(X1, X2, X3)) → if(proper(X1), proper(X2), proper(X3))
proper(diff(X1, X2)) → diff(proper(X1), proper(X2))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 6 less nodes.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesReductionPairsProof

              ↳ QDP

                ↳ Narrowing

                  ↳ QDP

                    ↳ Narrowing

                      ↳ QDP

                        ↳ DependencyGraphProof

                          ↳ QDP

                            ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

TOP(ok(diff(x0, x1))) → TOP(diff(active(x0), x1))
TOP(ok(diff(x0, x1))) → TOP(diff(x0, active(x1)))
TOP(ok(p(s(x0)))) → TOP(mark(x0))
TOP(mark(s(x0))) → TOP(s(proper(x0)))
TOP(ok(leq(x0, x1))) → TOP(leq(active(x0), x1))
TOP(ok(if(x0, x1, x2))) → TOP(if(active(x0), x1, x2))
TOP(ok(if(false, x0, x1))) → TOP(mark(x1))
TOP(ok(leq(x0, x1))) → TOP(leq(x0, active(x1)))
TOP(mark(diff(x0, x1))) → TOP(diff(proper(x0), proper(x1)))
TOP(mark(p(x0))) → TOP(p(proper(x0)))
TOP(ok(leq(s(x0), s(x1)))) → TOP(mark(leq(x0, x1)))
TOP(ok(s(x0))) → TOP(s(active(x0)))
TOP(ok(diff(x0, x1))) → TOP(mark(if(leq(x0, x1), 0, s(diff(p(x0), x1)))))
TOP(mark(if(x0, x1, x2))) → TOP(if(proper(x0), proper(x1), proper(x2)))
TOP(mark(leq(x0, x1))) → TOP(leq(proper(x0), proper(x1)))
TOP(ok(p(x0))) → TOP(p(active(x0)))
TOP(ok(if(true, x0, x1))) → TOP(mark(x0))

The TRS R consists of the following rules:

active(p(0)) → mark(0)
active(p(s(X))) → mark(X)
active(leq(0, Y)) → mark(true)
active(leq(s(X), 0)) → mark(false)
active(leq(s(X), s(Y))) → mark(leq(X, Y))
active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)
active(diff(X, Y)) → mark(if(leq(X, Y), 0, s(diff(p(X), Y))))
active(p(X)) → p(active(X))
active(s(X)) → s(active(X))
active(leq(X1, X2)) → leq(active(X1), X2)
active(leq(X1, X2)) → leq(X1, active(X2))
active(if(X1, X2, X3)) → if(active(X1), X2, X3)
active(diff(X1, X2)) → diff(active(X1), X2)
active(diff(X1, X2)) → diff(X1, active(X2))
diff(mark(X1), X2) → mark(diff(X1, X2))
diff(X1, mark(X2)) → mark(diff(X1, X2))
diff(ok(X1), ok(X2)) → ok(diff(X1, X2))
if(mark(X1), X2, X3) → mark(if(X1, X2, X3))
if(ok(X1), ok(X2), ok(X3)) → ok(if(X1, X2, X3))
leq(mark(X1), X2) → mark(leq(X1, X2))
leq(X1, mark(X2)) → mark(leq(X1, X2))
leq(ok(X1), ok(X2)) → ok(leq(X1, X2))
s(mark(X)) → mark(s(X))
s(ok(X)) → ok(s(X))
p(mark(X)) → mark(p(X))
p(ok(X)) → ok(p(X))
proper(p(X)) → p(proper(X))
proper(0) → ok(0)
proper(s(X)) → s(proper(X))
proper(leq(X1, X2)) → leq(proper(X1), proper(X2))
proper(true) → ok(true)
proper(false) → ok(false)
proper(if(X1, X2, X3)) → if(proper(X1), proper(X2), proper(X3))
proper(diff(X1, X2)) → diff(proper(X1), proper(X2))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

TOP(ok(p(s(x0)))) → TOP(mark(x0))

The remaining pairs can at least be oriented weakly.

TOP(ok(diff(x0, x1))) → TOP(diff(active(x0), x1))
TOP(ok(diff(x0, x1))) → TOP(diff(x0, active(x1)))
TOP(mark(s(x0))) → TOP(s(proper(x0)))
TOP(ok(leq(x0, x1))) → TOP(leq(active(x0), x1))
TOP(ok(if(x0, x1, x2))) → TOP(if(active(x0), x1, x2))
TOP(ok(if(false, x0, x1))) → TOP(mark(x1))
TOP(ok(leq(x0, x1))) → TOP(leq(x0, active(x1)))
TOP(mark(diff(x0, x1))) → TOP(diff(proper(x0), proper(x1)))
TOP(mark(p(x0))) → TOP(p(proper(x0)))
TOP(ok(leq(s(x0), s(x1)))) → TOP(mark(leq(x0, x1)))
TOP(ok(s(x0))) → TOP(s(active(x0)))
TOP(ok(diff(x0, x1))) → TOP(mark(if(leq(x0, x1), 0, s(diff(p(x0), x1)))))
TOP(mark(if(x0, x1, x2))) → TOP(if(proper(x0), proper(x1), proper(x2)))
TOP(mark(leq(x0, x1))) → TOP(leq(proper(x0), proper(x1)))
TOP(ok(p(x0))) → TOP(p(active(x0)))
TOP(ok(if(true, x0, x1))) → TOP(mark(x0))

Used ordering: Polynomial interpretation [25]:

POL(0) = 0
POL(TOP(x₁)) = x₁
POL(active(x₁)) = x₁
POL(diff(x₁, x₂)) = 0
POL(false) = 0
POL(if(x₁, x₂, x₃)) = x₂ + x₃
POL(leq(x₁, x₂)) = 0
POL(mark(x₁)) = x₁
POL(ok(x₁)) = x₁
POL(p(x₁)) = 1 + x₁
POL(proper(x₁)) = x₁
POL(s(x₁)) = x₁
POL(true) = 0

The following usable rules [17] were oriented:

p(mark(X)) → mark(p(X))
s(ok(X)) → ok(s(X))
proper(p(X)) → p(proper(X))
p(ok(X)) → ok(p(X))
leq(X1, mark(X2)) → mark(leq(X1, X2))
leq(mark(X1), X2) → mark(leq(X1, X2))
s(mark(X)) → mark(s(X))
leq(ok(X1), ok(X2)) → ok(leq(X1, X2))
diff(ok(X1), ok(X2)) → ok(diff(X1, X2))
diff(X1, mark(X2)) → mark(diff(X1, X2))
if(ok(X1), ok(X2), ok(X3)) → ok(if(X1, X2, X3))
if(mark(X1), X2, X3) → mark(if(X1, X2, X3))
active(diff(X1, X2)) → diff(active(X1), X2)
active(if(X1, X2, X3)) → if(active(X1), X2, X3)
diff(mark(X1), X2) → mark(diff(X1, X2))
active(diff(X1, X2)) → diff(X1, active(X2))
proper(false) → ok(false)
proper(if(X1, X2, X3)) → if(proper(X1), proper(X2), proper(X3))
proper(diff(X1, X2)) → diff(proper(X1), proper(X2))
proper(0) → ok(0)
proper(s(X)) → s(proper(X))
proper(leq(X1, X2)) → leq(proper(X1), proper(X2))
proper(true) → ok(true)
active(if(false, X, Y)) → mark(Y)
active(diff(X, Y)) → mark(if(leq(X, Y), 0, s(diff(p(X), Y))))
active(leq(s(X), s(Y))) → mark(leq(X, Y))
active(if(true, X, Y)) → mark(X)
active(leq(X1, X2)) → leq(active(X1), X2)
active(leq(X1, X2)) → leq(X1, active(X2))
active(p(X)) → p(active(X))
active(s(X)) → s(active(X))
active(leq(0, Y)) → mark(true)
active(leq(s(X), 0)) → mark(false)
active(p(0)) → mark(0)
active(p(s(X))) → mark(X)

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesReductionPairsProof

              ↳ QDP

                ↳ Narrowing

                  ↳ QDP

                    ↳ Narrowing

                      ↳ QDP

                        ↳ DependencyGraphProof

                          ↳ QDP

                            ↳ QDPOrderProof

                              ↳ QDP

                                ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

TOP(ok(diff(x0, x1))) → TOP(diff(active(x0), x1))
TOP(ok(diff(x0, x1))) → TOP(diff(x0, active(x1)))
TOP(mark(s(x0))) → TOP(s(proper(x0)))
TOP(ok(leq(x0, x1))) → TOP(leq(active(x0), x1))
TOP(ok(if(x0, x1, x2))) → TOP(if(active(x0), x1, x2))
TOP(ok(if(false, x0, x1))) → TOP(mark(x1))
TOP(ok(leq(x0, x1))) → TOP(leq(x0, active(x1)))
TOP(mark(diff(x0, x1))) → TOP(diff(proper(x0), proper(x1)))
TOP(mark(p(x0))) → TOP(p(proper(x0)))
TOP(ok(leq(s(x0), s(x1)))) → TOP(mark(leq(x0, x1)))
TOP(ok(s(x0))) → TOP(s(active(x0)))
TOP(ok(diff(x0, x1))) → TOP(mark(if(leq(x0, x1), 0, s(diff(p(x0), x1)))))
TOP(mark(if(x0, x1, x2))) → TOP(if(proper(x0), proper(x1), proper(x2)))
TOP(mark(leq(x0, x1))) → TOP(leq(proper(x0), proper(x1)))
TOP(ok(if(true, x0, x1))) → TOP(mark(x0))
TOP(ok(p(x0))) → TOP(p(active(x0)))

The TRS R consists of the following rules:

active(p(0)) → mark(0)
active(p(s(X))) → mark(X)
active(leq(0, Y)) → mark(true)
active(leq(s(X), 0)) → mark(false)
active(leq(s(X), s(Y))) → mark(leq(X, Y))
active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)
active(diff(X, Y)) → mark(if(leq(X, Y), 0, s(diff(p(X), Y))))
active(p(X)) → p(active(X))
active(s(X)) → s(active(X))
active(leq(X1, X2)) → leq(active(X1), X2)
active(leq(X1, X2)) → leq(X1, active(X2))
active(if(X1, X2, X3)) → if(active(X1), X2, X3)
active(diff(X1, X2)) → diff(active(X1), X2)
active(diff(X1, X2)) → diff(X1, active(X2))
diff(mark(X1), X2) → mark(diff(X1, X2))
diff(X1, mark(X2)) → mark(diff(X1, X2))
diff(ok(X1), ok(X2)) → ok(diff(X1, X2))
if(mark(X1), X2, X3) → mark(if(X1, X2, X3))
if(ok(X1), ok(X2), ok(X3)) → ok(if(X1, X2, X3))
leq(mark(X1), X2) → mark(leq(X1, X2))
leq(X1, mark(X2)) → mark(leq(X1, X2))
leq(ok(X1), ok(X2)) → ok(leq(X1, X2))
s(mark(X)) → mark(s(X))
s(ok(X)) → ok(s(X))
p(mark(X)) → mark(p(X))
p(ok(X)) → ok(p(X))
proper(p(X)) → p(proper(X))
proper(0) → ok(0)
proper(s(X)) → s(proper(X))
proper(leq(X1, X2)) → leq(proper(X1), proper(X2))
proper(true) → ok(true)
proper(false) → ok(false)
proper(if(X1, X2, X3)) → if(proper(X1), proper(X2), proper(X3))
proper(diff(X1, X2)) → diff(proper(X1), proper(X2))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

TOP(ok(diff(x0, x1))) → TOP(mark(if(leq(x0, x1), 0, s(diff(p(x0), x1)))))

The remaining pairs can at least be oriented weakly.

TOP(ok(diff(x0, x1))) → TOP(diff(active(x0), x1))
TOP(ok(diff(x0, x1))) → TOP(diff(x0, active(x1)))
TOP(mark(s(x0))) → TOP(s(proper(x0)))
TOP(ok(leq(x0, x1))) → TOP(leq(active(x0), x1))
TOP(ok(if(x0, x1, x2))) → TOP(if(active(x0), x1, x2))
TOP(ok(if(false, x0, x1))) → TOP(mark(x1))
TOP(ok(leq(x0, x1))) → TOP(leq(x0, active(x1)))
TOP(mark(diff(x0, x1))) → TOP(diff(proper(x0), proper(x1)))
TOP(mark(p(x0))) → TOP(p(proper(x0)))
TOP(ok(leq(s(x0), s(x1)))) → TOP(mark(leq(x0, x1)))
TOP(ok(s(x0))) → TOP(s(active(x0)))
TOP(mark(if(x0, x1, x2))) → TOP(if(proper(x0), proper(x1), proper(x2)))
TOP(mark(leq(x0, x1))) → TOP(leq(proper(x0), proper(x1)))
TOP(ok(if(true, x0, x1))) → TOP(mark(x0))
TOP(ok(p(x0))) → TOP(p(active(x0)))

Used ordering: Polynomial interpretation [25]:

POL(0) = 0
POL(TOP(x₁)) = x₁
POL(active(x₁)) = 0
POL(diff(x₁, x₂)) = 1
POL(false) = 0
POL(if(x₁, x₂, x₃)) = x₂ + x₃
POL(leq(x₁, x₂)) = 0
POL(mark(x₁)) = x₁
POL(ok(x₁)) = x₁
POL(p(x₁)) = 0
POL(proper(x₁)) = x₁
POL(s(x₁)) = 0
POL(true) = 0

The following usable rules [17] were oriented:

p(mark(X)) → mark(p(X))
s(ok(X)) → ok(s(X))
proper(p(X)) → p(proper(X))
p(ok(X)) → ok(p(X))
leq(X1, mark(X2)) → mark(leq(X1, X2))
leq(mark(X1), X2) → mark(leq(X1, X2))
s(mark(X)) → mark(s(X))
leq(ok(X1), ok(X2)) → ok(leq(X1, X2))
diff(ok(X1), ok(X2)) → ok(diff(X1, X2))
diff(X1, mark(X2)) → mark(diff(X1, X2))
if(ok(X1), ok(X2), ok(X3)) → ok(if(X1, X2, X3))
if(mark(X1), X2, X3) → mark(if(X1, X2, X3))
diff(mark(X1), X2) → mark(diff(X1, X2))
proper(false) → ok(false)
proper(if(X1, X2, X3)) → if(proper(X1), proper(X2), proper(X3))
proper(diff(X1, X2)) → diff(proper(X1), proper(X2))
proper(0) → ok(0)
proper(s(X)) → s(proper(X))
proper(leq(X1, X2)) → leq(proper(X1), proper(X2))
proper(true) → ok(true)

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesReductionPairsProof

              ↳ QDP

                ↳ Narrowing

                  ↳ QDP

                    ↳ Narrowing

                      ↳ QDP

                        ↳ DependencyGraphProof

                          ↳ QDP

                            ↳ QDPOrderProof

                              ↳ QDP

                                ↳ QDPOrderProof

                                  ↳ QDP

                                    ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

TOP(ok(diff(x0, x1))) → TOP(diff(active(x0), x1))
TOP(ok(diff(x0, x1))) → TOP(diff(x0, active(x1)))
TOP(mark(s(x0))) → TOP(s(proper(x0)))
TOP(ok(leq(x0, x1))) → TOP(leq(active(x0), x1))
TOP(ok(if(x0, x1, x2))) → TOP(if(active(x0), x1, x2))
TOP(ok(if(false, x0, x1))) → TOP(mark(x1))
TOP(ok(leq(x0, x1))) → TOP(leq(x0, active(x1)))
TOP(mark(diff(x0, x1))) → TOP(diff(proper(x0), proper(x1)))
TOP(mark(p(x0))) → TOP(p(proper(x0)))
TOP(ok(leq(s(x0), s(x1)))) → TOP(mark(leq(x0, x1)))
TOP(ok(s(x0))) → TOP(s(active(x0)))
TOP(mark(if(x0, x1, x2))) → TOP(if(proper(x0), proper(x1), proper(x2)))
TOP(mark(leq(x0, x1))) → TOP(leq(proper(x0), proper(x1)))
TOP(ok(p(x0))) → TOP(p(active(x0)))
TOP(ok(if(true, x0, x1))) → TOP(mark(x0))

The TRS R consists of the following rules:

active(p(0)) → mark(0)
active(p(s(X))) → mark(X)
active(leq(0, Y)) → mark(true)
active(leq(s(X), 0)) → mark(false)
active(leq(s(X), s(Y))) → mark(leq(X, Y))
active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)
active(diff(X, Y)) → mark(if(leq(X, Y), 0, s(diff(p(X), Y))))
active(p(X)) → p(active(X))
active(s(X)) → s(active(X))
active(leq(X1, X2)) → leq(active(X1), X2)
active(leq(X1, X2)) → leq(X1, active(X2))
active(if(X1, X2, X3)) → if(active(X1), X2, X3)
active(diff(X1, X2)) → diff(active(X1), X2)
active(diff(X1, X2)) → diff(X1, active(X2))
diff(mark(X1), X2) → mark(diff(X1, X2))
diff(X1, mark(X2)) → mark(diff(X1, X2))
diff(ok(X1), ok(X2)) → ok(diff(X1, X2))
if(mark(X1), X2, X3) → mark(if(X1, X2, X3))
if(ok(X1), ok(X2), ok(X3)) → ok(if(X1, X2, X3))
leq(mark(X1), X2) → mark(leq(X1, X2))
leq(X1, mark(X2)) → mark(leq(X1, X2))
leq(ok(X1), ok(X2)) → ok(leq(X1, X2))
s(mark(X)) → mark(s(X))
s(ok(X)) → ok(s(X))
p(mark(X)) → mark(p(X))
p(ok(X)) → ok(p(X))
proper(p(X)) → p(proper(X))
proper(0) → ok(0)
proper(s(X)) → s(proper(X))
proper(leq(X1, X2)) → leq(proper(X1), proper(X2))
proper(true) → ok(true)
proper(false) → ok(false)
proper(if(X1, X2, X3)) → if(proper(X1), proper(X2), proper(X3))
proper(diff(X1, X2)) → diff(proper(X1), proper(X2))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

TOP(ok(if(false, x0, x1))) → TOP(mark(x1))
TOP(ok(if(true, x0, x1))) → TOP(mark(x0))

The remaining pairs can at least be oriented weakly.

TOP(ok(diff(x0, x1))) → TOP(diff(active(x0), x1))
TOP(ok(diff(x0, x1))) → TOP(diff(x0, active(x1)))
TOP(mark(s(x0))) → TOP(s(proper(x0)))
TOP(ok(leq(x0, x1))) → TOP(leq(active(x0), x1))
TOP(ok(if(x0, x1, x2))) → TOP(if(active(x0), x1, x2))
TOP(ok(leq(x0, x1))) → TOP(leq(x0, active(x1)))
TOP(mark(diff(x0, x1))) → TOP(diff(proper(x0), proper(x1)))
TOP(mark(p(x0))) → TOP(p(proper(x0)))
TOP(ok(leq(s(x0), s(x1)))) → TOP(mark(leq(x0, x1)))
TOP(ok(s(x0))) → TOP(s(active(x0)))
TOP(mark(if(x0, x1, x2))) → TOP(if(proper(x0), proper(x1), proper(x2)))
TOP(mark(leq(x0, x1))) → TOP(leq(proper(x0), proper(x1)))
TOP(ok(p(x0))) → TOP(p(active(x0)))

Used ordering: Polynomial interpretation [25]:

POL(0) = 0
POL(TOP(x₁)) = x₁
POL(active(x₁)) = 0
POL(diff(x₁, x₂)) = 0
POL(false) = 0
POL(if(x₁, x₂, x₃)) = 1 + x₂ + x₃
POL(leq(x₁, x₂)) = 0
POL(mark(x₁)) = x₁
POL(ok(x₁)) = x₁
POL(p(x₁)) = 0
POL(proper(x₁)) = x₁
POL(s(x₁)) = 0
POL(true) = 0

The following usable rules [17] were oriented:

p(mark(X)) → mark(p(X))
s(ok(X)) → ok(s(X))
proper(p(X)) → p(proper(X))
p(ok(X)) → ok(p(X))
leq(X1, mark(X2)) → mark(leq(X1, X2))
leq(mark(X1), X2) → mark(leq(X1, X2))
s(mark(X)) → mark(s(X))
leq(ok(X1), ok(X2)) → ok(leq(X1, X2))
diff(ok(X1), ok(X2)) → ok(diff(X1, X2))
diff(X1, mark(X2)) → mark(diff(X1, X2))
if(ok(X1), ok(X2), ok(X3)) → ok(if(X1, X2, X3))
if(mark(X1), X2, X3) → mark(if(X1, X2, X3))
diff(mark(X1), X2) → mark(diff(X1, X2))
proper(false) → ok(false)
proper(if(X1, X2, X3)) → if(proper(X1), proper(X2), proper(X3))
proper(diff(X1, X2)) → diff(proper(X1), proper(X2))
proper(0) → ok(0)
proper(s(X)) → s(proper(X))
proper(leq(X1, X2)) → leq(proper(X1), proper(X2))
proper(true) → ok(true)

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesReductionPairsProof

              ↳ QDP

                ↳ Narrowing

                  ↳ QDP

                    ↳ Narrowing

                      ↳ QDP

                        ↳ DependencyGraphProof

                          ↳ QDP

                            ↳ QDPOrderProof

                              ↳ QDP

                                ↳ QDPOrderProof

                                  ↳ QDP

                                    ↳ QDPOrderProof

                                      ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

TOP(ok(diff(x0, x1))) → TOP(diff(active(x0), x1))
TOP(ok(diff(x0, x1))) → TOP(diff(x0, active(x1)))
TOP(mark(s(x0))) → TOP(s(proper(x0)))
TOP(ok(leq(x0, x1))) → TOP(leq(active(x0), x1))
TOP(ok(if(x0, x1, x2))) → TOP(if(active(x0), x1, x2))
TOP(ok(leq(x0, x1))) → TOP(leq(x0, active(x1)))
TOP(mark(diff(x0, x1))) → TOP(diff(proper(x0), proper(x1)))
TOP(mark(p(x0))) → TOP(p(proper(x0)))
TOP(ok(leq(s(x0), s(x1)))) → TOP(mark(leq(x0, x1)))
TOP(ok(s(x0))) → TOP(s(active(x0)))
TOP(mark(if(x0, x1, x2))) → TOP(if(proper(x0), proper(x1), proper(x2)))
TOP(mark(leq(x0, x1))) → TOP(leq(proper(x0), proper(x1)))
TOP(ok(p(x0))) → TOP(p(active(x0)))

The TRS R consists of the following rules:

active(p(0)) → mark(0)
active(p(s(X))) → mark(X)
active(leq(0, Y)) → mark(true)
active(leq(s(X), 0)) → mark(false)
active(leq(s(X), s(Y))) → mark(leq(X, Y))
active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)
active(diff(X, Y)) → mark(if(leq(X, Y), 0, s(diff(p(X), Y))))
active(p(X)) → p(active(X))
active(s(X)) → s(active(X))
active(leq(X1, X2)) → leq(active(X1), X2)
active(leq(X1, X2)) → leq(X1, active(X2))
active(if(X1, X2, X3)) → if(active(X1), X2, X3)
active(diff(X1, X2)) → diff(active(X1), X2)
active(diff(X1, X2)) → diff(X1, active(X2))
diff(mark(X1), X2) → mark(diff(X1, X2))
diff(X1, mark(X2)) → mark(diff(X1, X2))
diff(ok(X1), ok(X2)) → ok(diff(X1, X2))
if(mark(X1), X2, X3) → mark(if(X1, X2, X3))
if(ok(X1), ok(X2), ok(X3)) → ok(if(X1, X2, X3))
leq(mark(X1), X2) → mark(leq(X1, X2))
leq(X1, mark(X2)) → mark(leq(X1, X2))
leq(ok(X1), ok(X2)) → ok(leq(X1, X2))
s(mark(X)) → mark(s(X))
s(ok(X)) → ok(s(X))
p(mark(X)) → mark(p(X))
p(ok(X)) → ok(p(X))
proper(p(X)) → p(proper(X))
proper(0) → ok(0)
proper(s(X)) → s(proper(X))
proper(leq(X1, X2)) → leq(proper(X1), proper(X2))
proper(true) → ok(true)
proper(false) → ok(false)
proper(if(X1, X2, X3)) → if(proper(X1), proper(X2), proper(X3))
proper(diff(X1, X2)) → diff(proper(X1), proper(X2))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.